pp: Have PreprocessingPassContext derive from EnvObj. (#7127)

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 8a8bad20fa58efbcead3ab4aaa3d50c68efb1184..ac0301cc0cefc86b908bf2e1157c28203b096300 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -28,8 +28,8 @@ PreprocessingPassContext::PreprocessingPassContext(
     SmtEngine* smt,
     Env& env,
     theory::booleans::CircuitPropagator* circuitPropagator)
-    : d_smt(smt),
-      d_env(env),
+    : EnvObj(env),
+      d_smt(smt),
       d_circuitPropagator(circuitPropagator),
       d_llm(env.getTopLevelSubstitutions(),
             env.getUserContext(),
@@ -46,11 +46,6 @@ const LogicInfo& PreprocessingPassContext::getLogicInfo() const
   return d_env.getLogicInfo();
 }
 
-theory::Rewriter* PreprocessingPassContext::getRewriter() const
-{
-  return d_env.getRewriter();
-}
-
 theory::TrustSubstitutionMap&
 PreprocessingPassContext::getTopLevelSubstitutions() const
 {

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index b3a20d2b949391d52cc015ca14870c4572f7176d..29b2fda7f229220aac8cf8806f3c0f5b06a5cf94 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -24,6 +24,7 @@
 
 #include "context/cdhashset.h"
 #include "preprocessing/learned_literal_manager.h"
+#include "smt/env_obj.h"
 #include "theory/logic_info.h"
 #include "util/resource_manager.h"
 
@@ -33,10 +34,6 @@ class Env;
 class SmtEngine;
 class TheoryEngine;
 
-namespace theory {
-class Rewriter;
-}
-
 namespace theory::booleans {
 class CircuitPropagator;
 }
@@ -47,7 +44,7 @@ class PropEngine;
 
 namespace preprocessing {
 
-class PreprocessingPassContext
+class PreprocessingPassContext : protected EnvObj
 {
  public:
   /** Constructor. */
@@ -90,9 +87,6 @@ class PreprocessingPassContext
   /** Get the current logic info of the environment */
   const LogicInfo& getLogicInfo() const;
 
-  /** Get a pointer to the Rewriter owned by the associated Env. */
-  theory::Rewriter* getRewriter() const;
-
   /** Get a reference to the top-level substitution map */
   theory::TrustSubstitutionMap& getTopLevelSubstitutions() const;
 
@@ -137,8 +131,6 @@ class PreprocessingPassContext
  private:
   /** Pointer to the SmtEngine that this context was created in. */
   SmtEngine* d_smt;
-  /** Reference to the environment. */
-  Env& d_env;
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
   /**