From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 2 Sep 2021 16:43:29 +0000 (-0700)
Subject: Remove PreprocessingPassContext::getSmt().  (#7118)
X-Git-Tag: cvc5-1.0.0~1293
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d09af0b8789fd5e2a06032f93f85d0c9265a627;p=cvc5.git

Remove PreprocessingPassContext::getSmt().  (#7118)
---

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. */