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

diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 7d1c5bf54cb268df24960c34b34fcebe8f263205..7b93f43cfe8eb1b0a8af8cd6c92c44545be83715 100644 (file)
--- 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 f38f1e8239c879eacde0cd02659d01fd0f90f1d2..35c1a7fc20b2d85c4db0b0e13cd992b82ea7931d 100644 (file)
--- 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 65804b2b5452a8ae4c8da680e61e77f56cac4137..b3a20d2b949391d52cc015ca14870c4572f7176d 100644 (file)
--- 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. */