From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 3 Sep 2021 00:31:25 +0000 (-0700)
Subject: pp: Have PreprocessingPassContext derive from EnvObj. (#7127)
X-Git-Tag: cvc5-1.0.0~1281
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=973482b6da11d37a8aee96b98758f091f02008e5;p=cvc5.git

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

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 8a8bad20f..ac0301cc0 100644
--- 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 b3a20d2b9..29b2fda7f 100644
--- 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;
   /**