From 0e08fa4ff925b201d42544dd4b28c74d1b245bd7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Mar 2021 09:31:20 -0500 Subject: Move decision manager into theory inference manager (#6231) This makes it so that the decision manager is accessible from TheoryInferenceManager. This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes. --- src/theory/quantifiers_engine.cpp | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'src/theory/quantifiers_engine.cpp') diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 17a76468c..8d8f54768 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -51,7 +51,6 @@ QuantifiersEngine::QuantifiersEngine( : d_qstate(qstate), d_qim(qim), d_te(nullptr), - d_decManager(nullptr), d_pnm(pnm), d_qreg(qr), d_treg(tr), @@ -69,13 +68,12 @@ QuantifiersEngine::QuantifiersEngine( QuantifiersEngine::~QuantifiersEngine() {} -void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm) +void QuantifiersEngine::finishInit(TheoryEngine* te) { d_te = te; - 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_treg, dm, d_modules); + d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_treg, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); @@ -88,11 +86,6 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm) d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get()); } -DecisionManager* QuantifiersEngine::getDecisionManager() -{ - return d_decManager; -} - quantifiers::QuantifiersState& QuantifiersEngine::getState() { return d_qstate; -- cgit v1.2.3