From 8828e545cfb838d806a0ad382671a9af131e8431 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 Sep 2020 16:00:26 -0500 Subject: [PATCH] Minor cleanup of quantifiers engine (#4994) Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs. --- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 2 +- .../quantifiers/sygus/synth_conjecture.cpp | 4 +- src/theory/quantifiers/sygus_inst.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 28 +++++--- src/theory/quantifiers_engine.cpp | 66 ++++++++++--------- src/theory/quantifiers_engine.h | 19 ++++-- src/theory/theory_engine.cpp | 3 +- src/theory/theory_engine.h | 13 +--- 9 files changed, 75 insertions(+), 64 deletions(-) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index a771309f0..ab1bb16b5 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -205,7 +205,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) dlds = itds->second.get(); } // it is appended to the list of strategies - d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy( + d_quantEngine->getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds); return true; }else{ diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index d0536a1ea..7cc087b66 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -557,7 +557,7 @@ void CegisUnifEnumDecisionStrategy::initialize( } // register this strategy - d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( + d_qe->getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this); // create single condition enumerator for each decision tree strategy diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 5b7ad2049..52b24ac1a 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -235,7 +235,7 @@ void SynthConjecture::assign(Node q) d_feasible_guard, d_qe->getSatContext(), d_qe->getValuation())); - d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( + d_qe->getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); // this must be called, both to ensure that the feasible guard is // decided on with true polariy, but also to ensure that output channel @@ -255,7 +255,7 @@ void SynthConjecture::assign(Node q) { d_stream_strategy.reset(new SygusStreamDecisionStrategy( d_qe->getSatContext(), d_qe->getValuation())); - d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( + d_qe->getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_SYGUS_STREAM_FEASIBLE, d_stream_strategy.get()); d_current_stream_guard = d_stream_strategy->getLiteral(0); diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 56fee3319..ea5ff69e5 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -264,7 +264,7 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) d_quantEngine->getValuation()); d_dstrat[q].reset(ds); - d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy( + d_quantEngine->getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds); /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6e5dca4ef..bac67c7b6 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1091,15 +1091,25 @@ bool TermDb::reset( Theory::Effort effort ){ } ++eqcs_i; } - for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { - Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId]; - if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) { - context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - if ((*it).d_assertion.getKind() != INST_CLOSURE) - { - setHasTerm((*it).d_assertion); - } + TheoryEngine* te = d_quantEngine->getTheoryEngine(); + const LogicInfo& logicInfo = te->getLogicInfo(); + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) + { + if (!logicInfo.isTheoryEnabled(theoryId)) + { + continue; + } + Theory* theory = te->theoryOf(theoryId); + Assert(theory != nullptr); + for (context::CDList::const_iterator + it = theory->facts_begin(), + it_end = theory->facts_end(); + it != it_end; + ++it) + { + if ((*it).d_assertion.getKind() != INST_CLOSURE) + { + setHasTerm((*it).d_assertion); } } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index da60561ad..59082b55f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -172,39 +172,37 @@ class QuantifiersEnginePrivate } }; -QuantifiersEngine::QuantifiersEngine(context::Context* c, - context::UserContext* u, - TheoryEngine* te, +QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, ProofNodeManager* pnm) : d_te(te), + d_context(te->getSatContext()), + d_userContext(te->getUserContext()), + d_decManager(dm), d_masterEqualityEngine(nullptr), - d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), + d_eq_query( + new quantifiers::EqualityQueryQuantifiersEngine(d_context, this)), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), d_qepr(nullptr), d_term_util(new quantifiers::TermUtil(this)), d_term_canon(new expr::TermCanonize), - d_term_db(new quantifiers::TermDb(c, u, this)), + d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), - d_instantiate(new quantifiers::Instantiate(this, u, pnm)), - d_skolemize(new quantifiers::Skolemize(this, u)), + d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)), + d_skolemize(new quantifiers::Skolemize(this, d_userContext)), d_term_enum(new quantifiers::TermEnumeration), - d_conflict_c(c, false), - // d_quants(u), - d_quants_prereg(u), - d_quants_red(u), - d_lemmas_produced_c(u), - d_ierCounter_c(c), - // d_ierCounter(c), - // d_ierCounter_lc(c), - // d_ierCounterLastLc(c), - d_presolve(u, true), - d_presolve_in(u), - d_presolve_cache(u), - d_presolve_cache_wq(u), - d_presolve_cache_wic(u) + d_conflict_c(d_context, false), + d_quants_prereg(d_userContext), + d_quants_red(d_userContext), + d_lemmas_produced_c(d_userContext), + d_ierCounter_c(d_context), + d_presolve(d_userContext, true), + d_presolve_in(d_userContext), + d_presolve_cache(d_userContext), + d_presolve_cache_wq(d_userContext), + d_presolve_cache_wic(d_userContext) { // initialize the private utility d_private.reset(new QuantifiersEnginePrivate); @@ -217,7 +215,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, if (options::sygus() || options::sygusInst()) { - d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this)); + d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this)); } d_util.push_back(d_instantiate.get()); @@ -245,7 +243,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); bool needsBuilder = false; - d_private->initialize(this, c, d_modules, needsBuilder); + d_private->initialize(this, d_context, d_modules, needsBuilder); if (d_private->d_rel_dom.get()) { @@ -261,16 +259,18 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( - this, c, "FirstOrderModelFmc")); - d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this)); + this, d_context, "FirstOrderModelFmc")); + d_builder.reset( + new quantifiers::fmcheck::FullModelChecker(d_context, this)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_model.reset( - new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); - d_builder.reset(new quantifiers::QModelBuilder(c, this)); + new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel")); + d_builder.reset(new quantifiers::QModelBuilder(d_context, this)); } }else{ - d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); + d_model.reset( + new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel")); } } @@ -281,14 +281,18 @@ void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee) d_masterEqualityEngine = mee; } -context::Context* QuantifiersEngine::getSatContext() +TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; } + +DecisionManager* QuantifiersEngine::getDecisionManager() { - return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext(); + return &d_decManager; } +context::Context* QuantifiersEngine::getSatContext() { return d_context; } + context::UserContext* QuantifiersEngine::getUserContext() { - return d_te->theoryOf(THEORY_QUANTIFIERS)->getUserContext(); + return d_userContext; } OutputChannel& QuantifiersEngine::getOutputChannel() diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bd88034cb..72c0efce1 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -45,6 +45,7 @@ class TheoryEngine; namespace theory { +class DecisionManager; class QuantifiersEnginePrivate; // TODO: organize this more/review this, github issue #1163 @@ -56,14 +57,14 @@ class QuantifiersEngine { typedef context::CDHashSet NodeSet; public: - QuantifiersEngine(context::Context* c, - context::UserContext* u, - TheoryEngine* te, + QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, ProofNodeManager* pnm); ~QuantifiersEngine(); //---------------------- external interface /** get theory engine */ - TheoryEngine* getTheoryEngine() const { return d_te; } + TheoryEngine* getTheoryEngine() const; + /** Get the decision manager */ + DecisionManager* getDecisionManager(); /** get default sat context for quantifiers engine */ context::Context* getSatContext(); /** get default sat context for quantifiers engine */ @@ -121,7 +122,7 @@ class QuantifiersEngine { * precendence. */ std::map< Node, int > d_owner_priority; -public: + public: /** get owner */ QuantifiersModule * getOwner( Node q ); /** @@ -337,8 +338,14 @@ public: Statistics d_statistics; private: - /** reference to theory engine object */ + /** Pointer to theory engine object */ TheoryEngine* d_te; + /** The SAT context */ + context::Context* d_context; + /** The user context */ + context::UserContext* d_userContext; + /** Reference to the decision manager of the theory engine */ + DecisionManager& d_decManager; /** Pointer to the master equality engine */ eq::EqualityEngine* d_masterEqualityEngine; /** vector of utilities for quantifiers */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6a548e5b6..ac06d266d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -165,8 +165,7 @@ void TheoryEngine::finishInit() { if (d_logicInfo.isQuantified()) { // initialize the quantifiers engine - d_quantEngine = - new QuantifiersEngine(d_context, d_userContext, this, d_pnm); + d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm); } // initialize the theory combination manager, which decides and allocates the // equality engines to use for all theories. diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 167bd6d75..30b5d9fbb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -94,10 +94,6 @@ namespace eq { class EqualityEngine; } // namespace eq -namespace quantifiers { -class TermDb; -} - class EntailmentCheckParameters; class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ @@ -115,7 +111,6 @@ class TheoryEngine { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; friend class theory::CombinationEngine; - friend class theory::quantifiers::TermDb; friend class theory::EngineOutputChannel; friend class theory::CombinationEngine; @@ -373,16 +368,12 @@ class TheoryEngine { /** * Get a pointer to the underlying sat context. */ - inline context::Context* getSatContext() const { - return d_context; - } + context::Context* getSatContext() const { return d_context; } /** * Get a pointer to the underlying user context. */ - inline context::Context* getUserContext() const { - return d_userContext; - } + context::UserContext* getUserContext() const { return d_userContext; } /** * Get a pointer to the underlying quantifiers engine. -- 2.30.2