From 5712bdcd06a9f9502c3b5487386e1277702e25f4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Oct 2021 13:32:20 -0500 Subject: Make decision engine use env (#7300) --- src/prop/prop_engine.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'src/prop') diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 9060c318c..34dff2ba8 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -79,7 +79,6 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env) d_assumptions(d_env.getUserContext()) { Debug("prop") << "Constructing the PropEngine" << std::endl; - context::Context* satContext = d_env.getContext(); context::UserContext* userContext = d_env.getUserContext(); ProofNodeManager* pnm = d_env.getProofNodeManager(); ResourceManager* rm = d_env.getResourceManager(); @@ -88,17 +87,17 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env) if (dmode == options::DecisionMode::JUSTIFICATION || dmode == options::DecisionMode::STOPONLY) { - d_decisionEngine.reset(new decision::JustificationStrategy( - satContext, userContext, d_skdm.get(), rm)); + d_decisionEngine.reset( + new decision::JustificationStrategy(env, d_skdm.get())); } else if (dmode == options::DecisionMode::JUSTIFICATION_OLD || dmode == options::DecisionMode::STOPONLY_OLD) { - d_decisionEngine.reset(new DecisionEngineOld(satContext, userContext, rm)); + d_decisionEngine.reset(new DecisionEngineOld(env)); } else { - d_decisionEngine.reset(new decision::DecisionEngineEmpty(satContext, rm)); + d_decisionEngine.reset(new decision::DecisionEngineEmpty(env)); } d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry()); -- cgit v1.2.3