From 2d09af0b8789fd5e2a06032f93f85d0c9265a627 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 2 Sep 2021 09:43:29 -0700 Subject: [PATCH] Remove PreprocessingPassContext::getSmt(). (#7118) --- src/preprocessing/passes/sort_infer.cpp | 4 +--- src/preprocessing/preprocessing_pass.cpp | 8 ++++---- src/preprocessing/preprocessing_pass_context.h | 2 -- 3 files changed, 5 insertions(+), 9 deletions(-) diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 7d1c5bf54..7b93f43cf 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -20,7 +20,6 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/dump_manager.h" -#include "smt/smt_engine.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/theory_engine.h" @@ -72,8 +71,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( assertionsToPreprocess->push_back(nar); } // indicate correspondence between the functions - SmtEngine* smt = d_preprocContext->getSmt(); - smt::DumpManager* dm = smt->getDumpManager(); + smt::DumpManager* dm = d_env.getDumpManager(); for (const std::pair& mrf : model_replace_f) { dm->setPrintFuncInModel(mrf.first, false); diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index f38f1e823..35c1a7fc2 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -19,8 +19,8 @@ #include "preprocessing/preprocessing_pass_context.h" #include "printer/printer.h" #include "smt/dump.h" +#include "smt/env.h" #include "smt/output_manager.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "util/statistics_stats.h" @@ -45,9 +45,9 @@ void PreprocessingPass::dumpAssertions(const char* key, if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key)) { // Push the simplified assertions to the dump output stream - OutputManager& outMgr = d_preprocContext->getSmt()->getOutputManager(); - const Printer& printer = outMgr.getPrinter(); - std::ostream& out = outMgr.getDumpOut(); + Env& env = d_preprocContext->getEnv(); + const Printer& printer = env.getPrinter(); + std::ostream& out = env.getDumpOut(); for (const auto& n : assertionList) { diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 65804b2b5..b3a20d2b9 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -56,8 +56,6 @@ class PreprocessingPassContext Env& env, theory::booleans::CircuitPropagator* circuitPropagator); - /** Get the associated SmtEngine. */ - SmtEngine* getSmt() const { return d_smt; } /** Get the associated Environment. */ Env& getEnv() { return d_env; } /** Get the associated TheoryEngine. */ -- 2.30.2