diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-02 09:43:29 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-02 11:43:29 -0500 |
| commit | 2d09af0b8789fd5e2a06032f93f85d0c9265a627 (patch) | |
| tree | 4f8c73449f360ee29f83208fa25ae23f9a882b7a /src | |
| parent | ef80ba053b022ec624ee93a29a4dbc674226b3d4 (diff) | |
Remove PreprocessingPassContext::getSmt(). (#7118)
Diffstat (limited to 'src')
| -rw-r--r-- | src/preprocessing/passes/sort_infer.cpp | 4 | ||||
| -rw-r--r-- | src/preprocessing/preprocessing_pass.cpp | 8 | ||||
| -rw-r--r-- | 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<const Node, Node>& 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. */ |