Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)

This simplifies our management of how/when proofs are enabled in the PropEngine.

1 files changed, 7 insertions, 4 deletions

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index f988c00e2..0e54ff8c9 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -35,10 +35,12 @@
 
 namespace cvc5 {
 
+class Env;
+class TheoryEngine;
+
 namespace decision {
 class DecisionEngine;
 }
-class TheoryEngine;
 
 namespace prop {
 
@@ -56,9 +58,7 @@ class TheoryProxy : public Registrar
               TheoryEngine* theoryEngine,
               decision::DecisionEngine* decisionEngine,
               SkolemDefManager* skdm,
-              context::Context* context,
-              context::UserContext* userContext,
-              ProofNodeManager* pnm);
+              Env& env);
 
   ~TheoryProxy();
 
@@ -162,6 +162,9 @@ class TheoryProxy : public Registrar
 
   /** The skolem definition manager */
   SkolemDefManager* d_skdm;
+
+  /** Reference to the environment */
+  Env& d_env;
 }; /* class TheoryProxy */
 
 }  // namespace prop