diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-23 19:12:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-23 19:12:32 -0600 |
| commit | 854ab7e1adce90ebd822cc29ffabf5546d13f5cc (patch) | |
| tree | 96bcb318ada0448c73d293c0b99db7b98eb1e4c4 /src/theory/quantifiers_engine.cpp | |
| parent | 4c0dbb8ec7871ff114a9e66233cd8c8dd853f0b4 (diff) | |
Add interface to TheoryState for sort inference and facts (#5967)
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ec4cb7905..7046a8ef0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -41,16 +41,17 @@ QuantifiersEngine::QuantifiersEngine( d_qim(qim), d_te(nullptr), d_decManager(nullptr), + d_pnm(pnm), d_qreg(), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), - d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)), + d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg)), d_eq_query(nullptr), d_sygus_tdb(nullptr), d_instantiate( new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)), - d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)), + d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)), d_term_enum(new quantifiers::TermEnumeration), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()), @@ -113,15 +114,13 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm) d_decManager = dm; // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); - d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_modules); + d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, dm, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); } } -TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; } - DecisionManager* QuantifiersEngine::getDecisionManager() { return d_decManager; @@ -387,7 +386,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( Trace.isOn("quant-engine-assert") ){ Trace("quant-engine-assert") << "Assertions : " << std::endl; - getTheoryEngine()->printAssertions("quant-engine-assert"); + d_te->printAssertions("quant-engine-assert"); } //reset utilities |