From dfd844226c4cc6c6d2af78ef6291b0a9d087f4d4 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 18 Aug 2021 15:13:21 -0500
Subject: Make TheoryProxy use Env, simplify initialization of PropEngine
 (#7031)

This simplifies our management of how/when proofs are enabled in the PropEngine.
---
 src/prop/theory_proxy.h | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'src/prop/theory_proxy.h')

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
-- 
cgit v1.2.3