diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-03 16:00:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-03 16:00:26 -0500 |
commit | 8828e545cfb838d806a0ad382671a9af131e8431 (patch) | |
tree | a488c085adf0ba36b2d3a0d24b547c1a2eb29926 /src/theory/quantifiers_engine.cpp | |
parent | 31b3986ea297d54e828cd6c34e3689435ba63d7c (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 66 |
1 files changed, 35 insertions, 31 deletions
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() |