diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-02 17:31:25 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-02 19:31:25 -0500 |
commit | 973482b6da11d37a8aee96b98758f091f02008e5 (patch) | |
tree | 017ad5b122f91f89e101ebfa407b677220eedecd | |
parent | bc008131991c13bb635c9351942e1ef3f7e6f49b (diff) |
pp: Have PreprocessingPassContext derive from EnvObj. (#7127)
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 9 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 12 |
2 files changed, 4 insertions, 17 deletions
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; /** |